sys-order(es; Sys; f)
== a1, b1:E(Sys).
== a1 is f*(b1)
==  (a2, b2:E(Sys).
==  a2 is f*(b2)  (a1 <loc a2)  (a1 is f*(a2))  (loc(b1) = loc(b2))  (b1 <loc b2)) 

latex

---

clarification:

sys-order(es; Sys; f)
== a1:es-E-interface(es;Sys), b1:es-E-interface(es;Sys).
== fun-connected(es-E-interface(es;Sys);f;b1;a1)
==  (a2:es-E-interface(es;Sys), b2:es-E-interface(es;Sys).
==  fun-connected(es-E-interface(es;Sys);f;b2;a2)
==   es-locl(es; a1; a2)
==   (fun-connected(es-E-interface(es;Sys);f;a2;a1))
==   (es-loc(es; b1) = es-loc(es; b2)  Id)
==   es-locl(es; b1; b2)) 

latex

Up	abstract chain replication
Wellformedness Lemmas	sys-order wf
Definitions	x:A. B(x), A, y is f*(x), E(X), P  Q, s = t, Id, loc(e), (e <loc e')
FDL editor aliases	sys-order